$\forall$${\it es}$:ES, $l$:IdLnk, ${\it tg}$:Id, $A$:Type.
\\[0ex]($\forall$$e$:E. (kind($e$) = rcv($l$,${\it tg}$) $\in$ Knd) $\Rightarrow$ (valtype($e$) $\subseteq$r $A$))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. ($\uparrow$($e$ $\in_{b}$ es{-}in{-}port(${\it es}$;$l$;${\it tg}$))) $\Rightarrow$ ($\uparrow$isrcv($e$)))